M:(IdLnkIdType).
(x:IdLnk, x1:Id. AtomFree(Type;M(x,x1)))
 (l:IdLnk, tg:Id, v:M(l,tg). AtomFree(M(l,tg);v))
 (m:Msg(M). AtomFree(Msg(M);m)) 

latex

Definitions	x:A. B(x), P  Q, Msg(M), t  T, Prop, S  T, S  T
Lemmas	atom-free-IdLnk, atom-free-Id, IdLnk wf, Id wf, atom-free wf